Nuprl Lemma : p-first_wf
11,40
postcript
pdf
A
,
B
:Type,
L
:((
A
(
B
+ Top)) List). p-first(
L
)
A
(
B
+ Top)
latex
ProofTree
Definitions
Type
,
t
T
,
Top
,
left
+
right
,
x
:
A
B
(
x
)
,
type
List
,
Void
,
x
:
A
.
B
(
x
)
,
f
(
a
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
x
:
A
.
B
(
x
)
,
Unit
,
,
inr
x
,
x
,
y
.
t
(
x
;
y
)
,
list_accum(
x
,
a
.
f
(
x
;
a
);
y
;
l
)
,
x
.
A
(
x
)
,
p-first(
L
)
Lemmas
list
accum
wf
,
it
wf
,
top
wf
origin
A, B:Type, L:((A
(B + Top)) List). p-first(L) 
A(B + Top)
A, B:Type, L:((A(B + Top)) List). p-first(L) A(B + Top)
TB(x)
x:A.B(x)x:A. B(x)
x,y. t(x;y)x.A(x)